در اين مقاله قصد داريم مدل سطح بالايي بر پاية معادلات چندجملهاي با متغيرهاي صحيح ارائه دهيم كه مناسب براي وارسي خواص بر پاية CTL (Computational Temporal Logic) ميباشد. اكثر ابزارهاي وارسي از ساختمان دادههاي سطح پاييني مانند BDD استفاده ميكنند و اين ساختمان دادهها چکیده کامل
در اين مقاله قصد داريم مدل سطح بالايي بر پاية معادلات چندجملهاي با متغيرهاي صحيح ارائه دهيم كه مناسب براي وارسي خواص بر پاية CTL (Computational Temporal Logic) ميباشد. اكثر ابزارهاي وارسي از ساختمان دادههاي سطح پاييني مانند BDD استفاده ميكنند و اين ساختمان دادهها به علت نياز به حافظه زياد، قابل اعمال به بخش مسير داده از يك طرح نميباشند، در حالي كه مدل سطح بالاي پيشنهادی در اين مقاله قادر است بخشهاي مسير داده و كنترلر را با هم مورد ارزيابي قرار دهد. ضمن اينكه روش پيشنهادي به گونهاي است كه نياز به حل صريح معادلات نميباشد و اين كار توسط عمليات جايگزيني و سادهسازي انجام ميگيرد. در انتها نتايج كارمان با ابزار VIS، بعنوان يك ابزار وارسي بر پاية BDD، مقايسه ميگردند.
پرونده مقاله
